\section{Динамическая операционная\\
семантика языка L}

Состояния: $S=X\to\ZZ$ (частичная функция).

Нигде не определенное состояние: $\perp$.

Подстановка в состоянии: 

$$
s[x\gets z]=\lambda y.\left\{
                         \begin{array}{rcl}
                            z&,&y=x\\
                            s\; y&,&\mbox{иначе}
                         \end{array}
                      \right.
$$

\begin{itemize}
\item Семантика выражений: $\sembr{\bullet}:\fancy{E}\to(S\to\ZZ)$.

\begin{enumerate}
\item $\sembr{n}=\lambda s.n$, $n\in\NN$;
\item $\sembr{x}=\lambda s.s\;x$, $x\in X$;
\item $\sembr{A\otimes B}=\lambda s.\sembr{A}\;s\oplus\sembr{B}\;s$, где $\oplus$ ---
соответствующая $\otimes$ арифметическая операция.
\end{enumerate}

\item Семантика операторов. 

Множество конфигураций: $C=S\times\ZZ^*\times\ZZ^*$.

Правила перехода:

$$
\trans{c}{\llang{skip}}{c}\ruleno{Skip$_{bs}$}
$$

$$
\trans{\inbr{s,i,o}}{\mbox{$x\llang{:=}e$}}{\inbr{s[x\gets\sembr{e}\;s],i,o}}\ruleno{Assign$_{bs}$}
$$

$$
\trans{\inbr{s,zi,o}}{\mbox{$\llang{read}\;x$}}{\inbr{s[x\gets z],i,o}}\ruleno{Read$_{bs}$}
$$

$$
\trans{\inbr{s,i,o}}{\mbox{$\llang{write}\;e$}}{\inbr{s,i,o(\sembr{e}\;s)}}\ruleno{Write$_{bs}$}
$$

$$
\trule{\trans{c}{\mbox{$S_1$}}{c^\prime},\; \trans{c^\prime}{\mbox{$S_2$}}{c^{\prime\prime}}} 
      {\trans{c}{\mbox{$S_1\llang{;}S_2$}}{c^{\prime\prime}}}\ruleno{Seq$_{bs}$}
$$

$$
\crule{\trans{c}{\mbox{$S_1$}}{c^\prime}}
      {\trans{c}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}}
      {\sembr{e}\;s\ne 0}\ruleno{If-True$_{bs}$}
$$

$$
\crule{\trans{c}{\mbox{$S_2$}}{c^\prime}}
      {\trans{c}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}}
      {\sembr{e}\;s=0}\ruleno{If-False$_{bs}$}
$$

$$
\crule{\trans{c}{\llang{$S$}}{c^\prime},\;\trans{c^\prime}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}}
      {\trans{c}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}}
      {\sembr{e}\;s\ne 0}\ruleno{While-True$_{bs}$}
$$

$$
\ctrans{c}{\llang{while $\;e\;$ do $\;S\;$}}{c}{\sembr{e}\;s=0}\ruleno{While-False$_{bs}$}
$$


\item Семантика программы: $\sembr{\bullet}_P:\fancy{P}\to(\ZZ^*\to\ZZ^*)$.

$\sembr{P}_P=\lambda i.o$, где $\trans{\inbr{\perp,i,\epsilon}}{\llang{$P$}}{\inbr{s,\epsilon,o}}$
\end{itemize}

